MA:MsgA, s:MA.state, k:Knd, l:IdLnk, vaal:MA.V(k).
MA sends on link l  (filter(ms.eqof(IdLnkDeq)(mlnk(ms),l);MA.sends(k,s,vaal)) ~ nil) 

latex

Definitions	{i..j}, i  j < k, AB, (x  l), x:A. B(x), Prop, , ||as||, l[i], A & B, P  Q, map(f;as), 2of(t), x. t(x), P  Q, P & Q, deq-member(eq;x;L), product-deq(A;B;a;b), IdLnkDeq, S  T, EqDecider(T), KindDeq, Valtype(da;k), a:A fp B(a), x  dom(f), MsgA, M.state, Knd, IdLnk, M.V(k), M sends on link l, x:A. B(x), t  T, A, False, P  Q, b
Lemmas	ma-send-val-nil, ma-sends-on wf, assert wf, not wf, ma-v wf, IdLnk wf, Knd wf, ma-st wf, msga wf, deq wf, subtype rel self, Kind-deq wf, idlnk-deq wf, product-deq wf, deq-member wf, assert-deq-member, pi2 wf, map wf, select wf, length wf1, map length, le wf, map select